+(0, y) → y
+(s(x), y) → s(+(x, y))
-(0, y) → 0
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
↳ QTRS
↳ DependencyPairsProof
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(0, y) → 0
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
-1(s(x), s(y)) → -1(x, y)
+1(s(x), y) → +1(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(0, y) → 0
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
-1(s(x), s(y)) → -1(x, y)
+1(s(x), y) → +1(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(0, y) → 0
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
-1(s(x), s(y)) → -1(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(0, y) → 0
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
-1(s(x), s(y)) → -1(x, y)
The value of delta used in the strict ordering is 85/16.
POL(-1(x1, x2)) = x_1 + (13/4)x_2
POL(s(x1)) = 5/4 + (15/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(0, y) → 0
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
+1(s(x), y) → +1(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(0, y) → 0
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(s(x), y) → +1(x, y)
The value of delta used in the strict ordering is 1/2.
POL(s(x1)) = 1/4 + (7/2)x_1
POL(+1(x1, x2)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
+(0, y) → y
+(s(x), y) → s(+(x, y))
-(0, y) → 0
-(x, 0) → x
-(s(x), s(y)) → -(x, y)